$\forall$$T$:Type, $L$:($T$ List), $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$es\_realizer\{i:l\}), $A$:es\_realizer\{i:l\}.
\\[0ex]R{-}compat\{i:l\}(Rall($L$; $x$.$R$($x$)); $A$) $\Leftarrow\!\Rightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ R{-}compat\{i:l\}($R$($x$); $A$))